package main;

import java.awt.event.MouseEvent;
import java.awt.event.MouseListener;
import javax.swing.JTextArea;

/**
 * 
 * @author David Doyle
 *
 */
public class LawBar extends JTextArea {


	String currentText = "";

	/**
	 * This method initializes 
	 * @param width
	 * @param height
	 * 
	 * @author David Doyle
	 */
	public LawBar(int width, int height) {
		super();
		initialize(width,height);

		// Listener for the Text Area
		MouseListener ml =  new MouseListener(){
			@Override
			public void mouseClicked(MouseEvent arg0) {
			}

			@Override
			public void mouseEntered(MouseEvent arg0) {
			}

			@Override
			public void mouseExited(MouseEvent arg0) {
			}

			@Override
			public void mousePressed(MouseEvent arg0) {
			}

			@Override
			public void mouseReleased(MouseEvent arg0) {
			}
		};
		addMouseListener(ml);
	}

	/**
	 * This method initializes this
	 * 
	 * @author David Doyle
	 */
	private void initialize(int width, int height) {
		this.setSize(width, height);

		setText("0	Associative	[(X \u2261 (Y \u2261 Z)) \u2261 ((X \u2261 Y) \u2261 Z)]" +"\n"+
				"1	Symmetric	[X \u2261 Y \u2261 Y \u2261 X]" +"\n"+
				"2	Identity	[X \u2261 true \u2261 X]" +"\n"+
				"3	Reflexive	[X \u2261 X]" +"\n"+
				"4	True	true" +"\n"+
				"5	\u22C1 symmetric	[X \u22C1 Y \u2261 Y \u22C1 X]" +"\n"+
				"6	\u22C1 associative	[X \u22C1 (Y \u22C1 Z) \u2261 (X \u22C1 Y) \u22C1 Z]" +"\n"+
				"7	\u22C1 idempotent	[X \u22C1 X \u2261 X]" +"\n"+
				"8	\u22C1/\u2261	[X \u22C1 (Y \u2261 Z) \u2261 X \u22C1 Y \u2261 X \u2261 Z]" +"\n"+
				"9	\u22C1/\u22C1	[X \u22C1 (y \u22C1 Z) \u2261 (X \u22C1 Y) \u22C1 (X \u22C1 Z)]" +"\n"+
				"10	\u22C1	[X \u22C1 true \u2261 true]" +"\n"+
				"" +"\n"+
				"11	Golden Rule	[X \u22C0 Y \u2261 X \u2261 Y \u2261 X \u22C1 Y]" +"\n"+
				"12	\u22C0 symmetric	[X \u22C0 Y \u2261 Y \u22C0 X]" +"\n"+
				"13	\u22C0 associative	[X \u22C0 (Y \u22C0 Z) \u2261 (X \u22C1 Y) \u22C1 Z]" +"\n"+
				"14	\u22C0 idempotent	[X \u22C0 X \u2261 X)" +"\n"+
				"15	\u22C0 identity	[X \u22C0 true \u2261 X]" +"\n"+
				"16	abs\u22C1ption.0	[X \u22C0 (X \u22C1 Y) \u2261 X]" +"\n"+
				"17	abs\u22C1ption.1	[X \u22C1 (X \u22C0 Y) \u2261 X]" +"\n"+
				"18	\u22C1/\u22C0 	[X \u22C1 (Y \u22C0 Z) \u2261 (X \u22C1 Y] \u22C0 (X \u22C1 Z)]" +"\n"+
				"19	\u22C0/\u22C1	[X \u22C0 (Y \u22C1 Z) \u2261 (X \u22C0 Y) \u22C1 (X \u22C0 Z)]" +"\n"+
				"20	\u22C0 over \u2261	[X \u22C0 (Y \u2261 Z) \u2261 X \u22C0 Y \u2261 X \u22C0 Z \u2261 X]" +"\n"+
				"21	\u22C0/\u2261\u2261	[X \u22C0 (Y \u2261 Z \u2261 W) \u2261 X \u22C0 Y \u2261 X \u22C0 Z \u2261 X \u22C0 W]" +"\n"+
				"22	strong MP	[X \u22C0 (X \u2261 Y) \u2261 X \u22C0 Y]" +"\n"+
				"23	replacement	[(X \u2261 Y) \u22C0 (W \u2261 X) \u2261 (X \u2261 Y) \u22C0 (W \u2261 Y)]" +"\n"+
				"" +"\n"+
				"24	\u21D2 definition	[X \u21D2 Y \u2261 X \u22C0 Y \u2261 Y]" +"\n"+
				"25	\u21D2 reflexive	[X \u21D2 X]" +"\n"+
				"26	\u21D2 true	[X \u21D2 true]" +"\n"+
				"27	\u21D2 \u22C1	[X \u21D2 X \u22C1 Y]" +"\n"+
				"28	\u22C0 \u21D2	[X \u22C0 Y \u21D2 X]" +"\n"+
				"29	shunting	[X \u22C0 Y \u21D2 Z \u2261 X \u21D2 (Y \u21D2 Z)]" +"\n"+
				"30	\u21D2 to \u22C0 \u2261	[X \u21D2 Y \u2261 X \u22C0 Y \u2261 X]" +"\n"+
				"31	\u21D2 over \u2261	[X \u21D2 (Y \u2261 Z) \u2261 X \u22C0 Y \u2261 X \u22C0 Z]" +"\n"+
				"31a	\u21D2 distributes	[X \u21D2 (Y \u2261 Z) \u2261 X \u21D2 Y \u2261 X \u21D2 Z]" +"\n"+
				"33	\u22D0 definition	[X \u22D0 Y \u2261 X \u22C0 Y \u2261 Y]" +"\n"+
				"34	\u22D0\u21D2	[X \u22D0 Y \u2261 Y \u21D2 X]" +"\n"+
				"" +"\n"+
				"35	false definition	[false \u2261 \u00ACtrue]" +"\n"+
				"36	\u00AC over \u2261	[\u00AC(X \u2261 Y) \u2261 \u00ACX \u2261 Y]" +"\n"+
				"37	\u00AC flip	[\u00ACX \u2261 Y \u2261 X \u2261 \u00ACY]" +"\n"+
				"38	\u00AC\u00AC	[\u00AC\u00ACX \u2261 X]" +"\n"+
				"39	excluded middle	[X \u22C1 \u00ACX]" +"\n"+
				"40	\u00AC \u22C1 \u2261	[\u00ACX \u22C1 Y \u2261 X \u22C1 Y \u2261 Y]" +"\n"+
				"41	\u22C1 identity	[X \u22C1 false \u2261 X]" +"\n"+
				"42	\u22C0 zero	[X \u22C0 false \u2261 false]" +"\n"+
				"43	deM\u22C1gan.0	[\u00ACX \u22C1 \u00ACY \u2261 \u00AC(X \u22C0 Y)]" +"\n"+
				"44	\u00AC \u22C0 \u2261	[\u00ACX \u22C0 Y \u2261 X \u22C0 Y \u2261 \u00ACY]" +"\n"+
				"45	deM\u22C1gan.1	[\u00ACX \u22C0 \u00ACY \u2261 \u00AC(X \u22C1 Y)]" +"\n"+
				"46	complement.0	[X \u22C1 (\u00ACX \u22C0 Y) \u2261 X \u22C1 Y]" +"\n"+
				"47	complement.1	[X \u22C0 (\u00ACX \u22C1 Y) \u2261 X \u22C0 Y]" +"\n"+
				"48	\u2261 to \u22C0 \u22C1	[X \u2261 Y \u2261 (X \u22C0 Y) \u22C1 (\u00ACX \u22C0 \u00ACT)]" +"\n"+
				"49	contradiction	[X \u22C0 \u00ACX \u2261 false]" +"\n"+
				"50	\u21C1 to \u00AC \u22C1	[X \u21C1 Y \u2261 \u00ACX \u22C1 Y]" +"\n"+
				"51	contra-positive	[X \u21C1 Y \u2261 \u00ACY \u21C1 \u00ACX]" +"\n"+
				"52	false \u21C1	[false \u21C1 X]" +"\n"+
				"53	reducto ad absurdum	[X \u21C1 false \u2261 \u00ACX]" +"\n"+
				"54	\u00AC false 	[\u00ACfalse \u2261 true]" +"\n"+
				"55	MP	[X \u22C0(X \u21C1 Y) \u21C1 Y]" +"\n"+
				"56	mutual \u21C1	[X \u22C0 (X \u21C1 Y) \u22C0 (Y \u21C1 X) \u2261 X \u2261 Y]" +"\n"+
				"57	\u22C1 max	[(X \u21C1 Z) \u22C0 (Y \u21C1 Z) \u2261 X \u22C0 Y \u21C1 Z]" +"\n"+
				"58	\u22C0 min	[(X \u21C1 Y) \u22C0 (X \u21C1 Z) \u2261 X \u21C1 Y \u22C0 Z]" +"\n"+
				"" +"\n"+
				"59	\u2262 definition	[(X \u2262 Y) \u2261 not(X \u2261 Y)]" +"\n"+
				"60	\u2262 associative	[((X \u2262 Y) \u2262 Z) \u2261 Z) \u2261 (X \u2262 (Y \u2262 Z))]" +"\n"+
				"**61	\u2262 \u22C0 \u2261 associate	[((X \u2262 Y) \u2261 Z) \u2261 (X \u2262 (Y \u2262 Z))]" +"\n"+
				"**62	\u2262 \u22C0 \u2261 swap	[X \u2261 Y \u2262 Z \u2261 X \u2262 Y \u2261 Z]" +"\n"+
				"63	\u2262 symmetric	[X \u2262 Y \u2261 Y \u2262 X]" +"\n"+
				"64	\u2262 identity	[X \u2262 false \u2261 X]" +"\n"+
				"65	\u22C0/\u2262	[X \u22C0 (Y \u2262 Z) \u2261 X \u22C0 Y \u2262 X \u22C0 Z]" +"\n"+
				"" +"\n"+
				"66	\u21D2 transitive	[(X \u21D2 Y) \u22C0 (Y \u21D2 Z) \u21D2 (X \u21D2 Z)]" +"\n"+
				"67	\u22C1 monotonic	[(X \u21D2 Y) \u21D2 (X \u22C1 Z \u21D2 Y \u22C1 Z)]" +"\n"+
				"68	\u22C0 monotonic	[(X \u21D2 Y) \u21D2 (X \u22C0 Z \u21D2 Y \u22C0 Z)]" +"\n"+
				"69	\u21D2 anti-monotonic in antecedent	[(X \u21D2 Y) \u21D2 ((X \u21D2 Z) \u21D0 (Y \u21D2 Z))]" +"\n"+
				"70	\u2261 transitive	[(X \u2261 Y) \u22C0 (Y \u2261 Z) \u21D2 (X \u2261 Z)]" +"\n"+
				"" +"\n"+
				"100	trading	[<\u2200 i; r.i: f.i> \u2261 <\u2200 i;; not r.i \u22C1 f.i>]" +"\n"+
				"100a	trading	[<\u2200 i; r.i: f.i> \u2261 <\u2200 i;; r.i \u21D2 f.i>]" +"\n"+
				"101	\u22C1/\u2200	[X \u22C1 <\u2200 i: r.i: f.i> \u2261 <\u2200 i: r.i: X \u22C1 f.i>]" +"\n"+
				"102	\u2200/\u22C0	[<\u2200 i: r.i: f.i> \u22C0 <\u2200 i: r.i: g.i> \u2261 <\u2200 i: r.i: f.i \u22C0 g.i>]" +"\n"+
				"103	range split	[<\u2200 i: r.i: f.i> \u22C0 <\u2200 i: s.i: f.i:> \u2261 <\u2200 i: r.i \u22C1 s.t: f.i>]" +"\n"+
				"104	false range	[<\u2200 i: false: f.i> \u2261 true]" +"\n"+
				"105	1-point	[<\u2200 i: i=j: f.i> \u2261 f.j]" +"\n"+
				"106	instantiation	[<\u2200 i :: f.i> implies f.j>]" +"\n"+
				"" +"\n"+
				"107	\u2203 definition	[<\u2203 i: r.i: f.i> \u2261 not<\u2200 i: r.t: not f.i>]" +"\n"+
				"108	trading	[<\u2203 i: r.i: f.i> \u2261 <\u2203 i:: r.i \u22C0 f.i>]" +"\n"+
				"109	\u22C0/\u2203	X \u22C0 <\u2203 i: r.i: f.i> \u2261 <\u2203 i: r.t: X \u22C0 f.i>]" +"\n"+
				"110	\u2203/\u22C1	[<\u2203 i: r.i: f.i> \u22C1 <\u2203 i: r.i; g.i> \u2261 <\u2203 i: r.i: f.i \u22C1 g.i>]" +"\n"+
				"111	range split	[<\u2203 i: r.i: f.i> \u22C1 <\u2203 i: s.i: f.i> \u2261 <\u2203 i: r.i \u22C1 s.i: f.i>]" +"\n"+
				"122	false range	[<\u2203 i: false: f.i> \u2261 false]" +"\n"+
				"123	1-point	[<\u2203 i: i = j: f.i> \u2261 f.j]" +"\n"+
				"124	witness	[<\u2203 i :: f.i> bimply f.i]" +"\n"+
				"" +"\n"+
				"0*	[n \u2264 \u23BF x \u23CC \u2261 n \u2264 x]" +"\n"+
				"1	[\u23BF x \u23CC \u2264 x]" +"\n"+
				"2	[n \u2264 \u23BF n \u23CC]" +"\n"+
				"3	[\u23BF n \u23CC \u2264 n]" +"\n"+
				"4	[n = \u23BF n \u23CC]" +"\n"+
				"5	[\u23BF x \u23CC < n \u2261 x < n]" +"\n"+
				"6	[x < \u23BF x \u23CC + 1]" +"\n"+
				"7	[\u23BF x \u23CC \u2264 x \u22C0 x < \u23BF x \u23CC + 1]" +"\n"+
				"8	[\u23BF x \u23CC \u2264 \u23BF y \u23CC < \u23BF x \u23CC + 1]" +"\n"+
				"9	[\u23BF x \u23CC + n \u2261 \u2264 x \u22C0 x < n + 1]" +"\n"+
				"10	[\u23BF x \u23CC + n \u2261 x - 1 < n \u22C0 n \u2264 x]" +"\n"+
				"11	[\u23BF x + n \u23CC = \u23BF x \u23CC + n]" +"\n"+
				"" +"\n"+
				"12*	[\u23BE n \u23CB \u2264 x \u2261 n \u2264 x]" +"\n"+
				"13	[x \u2264 \u23BE x \u23CB]" +"\n"+
				"14	[\u23BE n \u23CB \u2264 n]" +"\n"+
				"15	[n \u2264 \u23BE n \u23CB]" +"\n"+
				"16	[n = \u23BE n \u23CB]" +"\n"+
				"17	[n < \u23BE x \u23CB \u2261 x < n]" +"\n"+
				"18	[\u23BE x \u23CB - 1 < x]" +"\n"+
				"19	[\u23BE x \u23CB -1 < x \u22C0 x < \u23BE x \u23CB]" +"\n"+
				"20	[\u23BE x \u23CB \u2264 \u23BE y \u23CB \u21D2 x \u2264 y]" +"\n"+
				"21	[\u23BE x \u23CB = n \u2261 n - 1 < x \u22C0 x \u2264 n]" +"\n"+
				"22	[\u23BE x \u23CB = n \u2261 x \u2264 n \u22C0 n < x + 1]" +"\n"+
				"23	[\u23BE x + n \u23CB = \u23BE x \u23CB + n]"
				);



	}

	/**
	 * Updates the currentText variable with the contents of the text area
	 * (possible solution for file I/O and recovery)
	 * 
	 * @author Balazs Pete
	 */
	public void updateText(){
		currentText = this.getText();
		//Remove // to see result in console..
		//System.out.println(currentText);
	}

	
}  //  @jve:decl-index=0:visual-constraint="99,17"
